$\forall$$A$:Type, $a$:($A$ List), $b$:(\{${\it a@}_{0}$:$A$$\mid$ (${\it a@}_{0}$ $\in$ $a$)\} $\rightarrow$Top). mkfpf($a$;$b$) $\in$ $a$:$A$ fp$\rightarrow$ Top